% vim: set fdm=marker: sw=2: sts=2: ts=2:

\section{Prenexné tvary formúl}

Ako sme mali vo výrokovej logike isté normálne tvary - konjunktívnu a
disjunktívnu normálnu formu, budeme mať aj v predikátovej logike isté
špeciálne tvary. Zaujímavé sú najmä prexenxná forma a ešte Skolemov
normálny tvar, čo je špeciálny prípad prexenej formy.
V prípade prenexného tvaru ide o preskupenie kvantifikátorov na
začiatok formuly -- tvar vzniká aplikovaním kvantifikátorov na otvorenú
formulu.


\begin{definicia}[Prenexný tvar]
    Formula $A$ je v prenexnom tvare, ak $A$ je v nasledujúcom tvare:
    \begin{equation*}
     (Q_1 x_1) (Q_2 x_2) (Q_3 x_3) \dots (Q_n x_n) B
    \end{equation*}
    kde $x_1, \dots , x_n$ sú navzájom rôzne premenné,
    $Q_i \in\{\forall, \exists\}$ sú
    kvantifikátory a  formula $B$ je bez kvantifikátorov.
    Formulu $B$ nazveme otvoreným jadrom formuly $A$, 
    výraz $(Q_1 x_1) (Q_2 x_2) (Q_3 x_3) \dots (Q_n x_n)$ nazveme
    prefixom formuly $A$.
\end{definicia}

\begin{poznamka}
    \noindent
    \begin{itemize}
     \item $x_1, \dots, x_n$ sú navzájom rôzne pre vylúčenie viacnásobných
        kvantifikácií.
     \item Ak $n=0$, tak $A$ je otvorená a nemá prefix.
     \item $B$ je najväčšia otvorená podformula formuly $A$.
    \end{itemize}
\end{poznamka}

\begin{priklad}
    Nasledujúca formula elementárnej aritmetiky je v prenexnom tvare:
    \begin{equation*}
        (\forall x) (\forall y) (\exists z) (x+y=z)
    \end{equation*}
    Prefixom je $(\forall x)(\forall y)(\exists z)$ a otvorené jadro
    je $x+y=z$.
\end{priklad}

\begin{veta}
 Nech $A$ je ľubovoľná formula predikátovej logiky. Potom existuje
 formula $A'$ v prenexnom tvare taká, že
 $\provable A \lequiv A'$.
 \label{veta:prenex}
\end{veta}

Pri prevádzaní formuly na prenexný tvar budeme využívať nasledujúce
{\it prenexné operácie}, každá z nich nahrádza podformulu
jej ekvivalentom.
\begin{itemize}
    \item[a)] Podformulu $B$ nahraď jej variantom (premenovanie viazaných
        premenných).

    \item[b)] $\neg(Q x) B$ nahraď $(\overline{Q} x) \neg B$
        (negácia kvantifikátorov).

    \item[c)] ak $x$ nie je voľná v $B$, tak podformulu $B\implies (Qx)C$
            nahraď podformulou $(Qx) (B\implies C)$.

    \item[d)] ak $x$ nie je voľná v $C$, tak $((Qx) B) \implies C$
        nahraď $(\overline{Q} x) (B \implies C)$.

    \item[e)] ak $x$ nie je voľná v $B$ resp. $C$, $\square \in \{\land,\lor\}$.
     Potom $B \squareop ((Qx)C)$ resp. $((Qx)B)\squareop C$ nahraď
     $(Qx)(B \squareop C)$.
\end{itemize}
\begin{poznamka}
    Asi stojí za zmienku upozorniť, že v časti d) $x$ nie je voľná vo
    formule $C$ narozdiel od časti c), kde $x$ nie je voľná v $B$.
    Taktiež, medzi týmito dvoma prípadmi je zásadný rozdiel v
    tom, že v časti d) negujeme kvantifikátor.
\end{poznamka}

\begin{lema}
    Prenexnými operáciami dostaneme ekvivalentné formuly
\end{lema}
\begin{dokaz}
  %%% {{{ 
  \noindent
  \begin{itemize}
    \item[a)] Veta o variantoch

    \item[b)] Platí
        %%% {{{
        \begin{itemize}
        \item[1]
            $\provable \neg(\forall x) B \lequiv
                \highlighto{
                \neg (\forall x) \highlightb{\neg\neg} B}$ -- 
                pretože platí $B \lequiv \neg \neg B$

        \item[2]
            $\provable \highlighto{
                \highlighta{\neg (\forall x) \neg} \neg B}
             \lequiv \highlightb{(\exists x)} \neg B$ --
                pretože $(\exists x) A$ je z definície
                $\neg (\forall x) \neg A$.
        \end{itemize}
        Následným použítím vety o ekvivalencii môžeme prvú
        ekvivalenciu dosadiť do druhej a dostávame požadovaný
        výsledok.
        Podobne
        \begin{itemize}
        \item[1]
            $\provable \neg(\exists x) B \lequiv
                \highlighto{
                \neg (\exists x) \highlightb{\neg\neg} B}$

        \item[2]
            $\provable \highlighto{
                \highlighta{\neg (\exists x) \neg} \neg B}
                \lequiv \highlightb{(\forall x)} \neg B$
        \end{itemize}
        %%% }}}

    \item[c)]
        %%% {{{
        Nech $Q=\forall$. Chceme ukázať
        $\provable (\forall x) (B \implies C) \lequiv
            (B \implies (\forall x) C)$ kde $x$ nie je voľná v $B$.
        \begin{itemize}
        \item[$\Rightarrow$]
            Piata axióma predikátovej logiky.


        \item[$\Leftarrow$]
            \begin{itemize}
            %%% {{{
            \item[1] $\provable (\forall x) C \implies C$ --
                axióma špecifikácie

            \item[2] $\provable \highlighta{
                 \underbrace{(B \implies (\forall x) C)}_X
                \implies 
                 [\underbrace{((\forall x) C \implies C)}_Y
                    \implies \underbrace{(B \implies C)}_Z]}$ --
                    Jednoduchý sylogizmus

            \item[*] $\provable X \implies (Y \implies Z)$.

            \item[*] $\provable (X \implies (Y \implies Z)) \implies
                (Y \implies (X \implies Z))$ -- pravidlo zámeny
                predpokladov

            \item[3] $\provable \highlighta{
                [(B \implies (\forall x) C)
                \implies 
                 (((\forall x) C \implies C)
                    \implies (B \implies C))]
                }
                \implies \highlightb{
                   [((\forall x) C \implies C) \implies
                    ((B \implies (\forall x) C) \implies (B \implies
                    C))]}$.

            \item[4] $\provable
                  \highlightb{
                   ((\forall x) C \implies C) \implies
                    \highlighto{
                    [(B \implies (\forall x) C) \implies (B \implies
                    C)]}}$ - MP 2,3

            \item[5] $\provable \highlighto{
                (B \implies (\forall x) C) \implies (B
                    \implies C)}$ - MP 1,4

            \item[6] $\provable (B \implies (\forall x) C) \implies
                \highlighta{(\forall x)} (B \implies C)$ -- 
                pravidlo zavedenia veľkého kvantifikátora
            %%% }}}
            \end{itemize}
        \end{itemize}

        Druhou možnosťou je $Q=\exists$. Našim cieľom je ukázať
        $\provable (\exists x) (B \implies C) \lequiv 
        (B \implies (\exists x) C)$ za predpokladu že $x$ nie je voľná v $B$.
        \begin{itemize}
        \item[$\Rightarrow$]
            \begin{itemize}
            %%% {{{
            \item[1] $\provable C \implies (\exists x) C$ --
                duálna verzia axiómy špecifikácie

            \item[2] $\provable (B \implies C) \implies
                 ((C \implies (\exists c) C) \implies (B \implies
                 (\exists x) C ))$ -- jednoduchý sylogizmus (JS)

            \item[3] $\provable
                \highlighta{
                [(B \implies C) \implies (( C \implies (\exists x) C)
                \implies (B \implies (\exists x) C))]}
                \implies
                \highlightb{
                  [(C \implies (\exists x) C) \implies (( B \implies
                  C) \implies (B \implies (\exists x) C))]}$ -- 
                  pravidlo zámeny predpokladov

            \item[4] $\provable \highlightb{
                  ((C \implies (\exists x) C) \implies 
                  \highlighto{[( B \implies
                  C) \implies (B \implies (\exists x) C)]}}$ -- MP 2,3

            \item[5] $\provable
                  \highlighto{( B \implies
                  C) \implies (B \implies (\exists x) C)}$ -- MP 1,4

            \item[6] $\provable \highlighta{(\exists x)}
                ( B \implies C) \implies (B \implies (\exists x) C)$
                -- pravidlo zavedenie existenčného kvantifikátora
            %%% }}}
            \end{itemize}

        \medskip
        \item[$\Leftarrow$]
            \begin{itemize}
            %%% {{{
                \item[1] $\provable C \implies (B \implies C)$ -- A1

                \item[2] $\provable (\exists x) C \implies 
                    (\exists x)(B \implies C)$ -- pravidlo
                    distribúcie kvantifikátorov

                \item[3] $\provable \neg B \implies (B \implies C)$ -- postova
                teoréma

                \item[4] $\provable (B \implies C) \implies 
                    (\exists x)(B \implies C)$ -- 
                    duálny tvar axiómy špecifikácie

                \item[5] $\provable \highlighta{\neg B \implies 
                    (\exists x) (B \implies C)}$ -- JS 3,4

                \item[*] $\provable
                    \highlighta{
                    [\underbrace{\neg B\phantom{)}}_{\neg X} \implies 
                        \underbrace{(\exists x) ( B \implies C)}_Z]
                    }
                    \implies
                    \highlightb{
                    [(\underbrace{(\exists x) C}_Y 
                        \implies 
                      \underbrace{(\exists x) (B \implies C)}_Z)
                    \implies
                    ((\underbrace{B\phantom{)}}_X \implies 
                        \underbrace{(\exists x) C}_Y)
                      \implies 
                        \underbrace{(\exists x) (B
                    \implies C)}_Z)]}$ -- dokážeme neskôr

                \item[6] $\provable
                    \highlightb{
                    [(\exists x) C \implies (\exists x) (B \implies C)]
                    \implies
                    \highlighto{
                    [(B \implies (\exists x) C) \implies (\exists x) (B
                    \implies C ))]}}$ -- MP 5,*

                \item[7] $\provable
                    \highlighto{
                    (B \implies (\exists x) C) \implies (\exists x) (B
                    \implies C ))}$ -- MP 2,6
            %%% }}}
            \end{itemize}
            Ešte treba dokázať formulu (*)
            \begin{itemize}
            %%% {{{
            \item[a] $\neg X \implies Z, Y \implies Z, X \implies Y,
                \highlighta{X}
                \provable Z$
            \item[b] $\neg X \implies Z, Y \implies Z, X \implies Y,
                \highlightb{\neg X}
                \provable Z$
            \item[c] $\neg X \implies Z, Y \implies Z, X \implies Y
                \provable Z$ -- veta o neutrálnej formule ($X,\neg
                X$).
            \item[d] $\provable (\neg X \implies Z) \implies (
                    (Y \implies Z) \implies ((X \implies Y) \implies
                    Z))$ -- veta o dedukcii
            %%% }}}
            \end{itemize}
        \end{itemize}
        %%% }}}

    \item[d)]
        %%% {{{
        \begin{itemize}
        \item $Q=\forall$: Ukazujeme
            $\provable (\exists x) (B \implies C) \lequiv
             ((\forall x) B \implies C)$ ak $x$ nie je voľná v $C$.
            \begin{itemize}
            %%% {{{
            \item[1]
                $\provable \highlightc{((\forall x) B \implies C)}
                    \lequiv
                    (\neg C \implies \neg (\forall x) B)$
            \item[2]
                $\provable \highlightc{((\forall x) B \implies C)}
                    \lequiv
                    (\neg C \implies \neg (\forall x) \highlighta{\neg
                    \neg} B)$
            \item[3]
                $\provable \highlightc{((\forall x) B \implies C)}
                    \lequiv
                    \highlightp{
                    (\neg C \implies \highlightb{(\exists x)} \neg B)}$
            \item[4]
                $\provable 
                    \highlighto{(\exists x) (\neg C \implies \neg B)}
                \lequiv
                    \highlightp{
                    (\neg C \implies (\exists x) \neg B)}$
                 -- časť c) tohoto dôkazu

            \item[5]
                $\provable \highlightc{((\forall x) B \implies C)}
                    \lequiv
                    \highlighto{(\exists x) 
                        (\highlightb{\neg C \implies \neg B)}}$ --
                    vetou o ekvivalentných zámenách sme dosadili 4 do 3
            \item[6] 
                $\provable (\highlighta{B\implies C}) 
                    \lequiv 
                    (\highlightb{\neg C \implies \neg B})$ -- 
                    vieme z výrokovej logiky
            \item[7]
                $\provable \highlightc{((\forall x) B \implies C)}
                    \lequiv
                    (\exists x) (\highlighta{B \implies C})$ --
                    použili sme vetu o ekvivalentných zámenách na
                    5,6.
            %%% }}}
            \end{itemize}

        \item $Q=\exists$: Chceme ukázať
            $\provable (\exists x) (B \implies C) \lequiv
             ((\forall x) B \implies C)$ ak $x$ nie je voľná v $B$.
             Postupujeme analogicky ako v predchádzajúcom prípade
            \begin{itemize}
            %%% {{{
            \item[1]
                $\provable \highlightc{((\exists x) B \implies C)}
                    \lequiv
                    (\neg C \implies \neg (\exists x) B)$
            \item[2]
                $\provable \highlightc{((\exists x) B \implies C)}
                    \lequiv
                    (\neg C \implies \neg (\exists x) \highlighta{\neg
                    \neg} B)$
            \item[3]
                $\provable \highlightc{((\exists x) B \implies C)}
                    \lequiv
                    \highlightp{
                    (\neg C \implies \highlightb{(\forall x)} \neg B)}$
            \item[4]
                $\provable 
                    \highlighto{(\forall x) (\neg C \implies \neg B)}
                \lequiv
                    \highlightp{
                    (\neg C \implies (\forall x) \neg B)}$
                 -- časť c) tohoto dôkazu

            \item[5]
                $\provable \highlightc{((\exists x) B \implies C)}
                    \lequiv
                    \highlighto{(\forall x) 
                        (\highlightb{\neg C \implies \neg B)}}$ --
                    vetou ekvivalentných zámenách sme dosadili 4 do 3
            \item[6] 
                $\provable (\highlighta{B\implies C}) 
                    \lequiv 
                    (\highlightb{\neg C \implies \neg B})$ -- 
                    vieme z výrokovej logiky
            \item[7]
                $\provable \highlightc{((\exists x) B \implies C)}
                    \lequiv
                    (\forall x) (\highlighta{B \implies C})$ --
                    použili sme vetu o ekvivalentných zámenách na
                    5,6.
            %%% }}}
            \end{itemize}
        \end{itemize}
        %%% }}}

    \item[e)] Ukazujeme
        $\provable (Qx) (B\squareop C) \lequiv (B\squareop (Qx)C)$,
        kde $x$ nie je voľná v $B$.
        Na základe operácii c), d) toto vieme dokázať, pretože platí
        \begin{align*}
            &\provable (A \lor B) \lequiv (\neg A \implies B) \\
            &\provable (A \land B) \lequiv \neg(A \implies \neg B)
        \end{align*}

  \end{itemize}
  %%% }}}
\end{dokaz}

\begin{dokaz}[Dôkaz vety \ref{veta:prenex} o prexexných tvaroch]
%%% {{{
Budeme postupovať matematickou indukciou vzhľadom na zložitosť formuly $A$.
\begin{itemize}
    \item $A$ je atomická formula. Potom je $A$ v prenexnom tvare.

    \item $A=\neg B$. Na $B$ sa vzťahuje IP, teda vieme zostrojiť
        $B'$ takú, že platí
        $\provable B \lequiv B'$.
        Položíme $A'=\neg B'$ a niekoľkonásobným aplikovaním 
        prenexnej operácie b) dostaneme 
        $A''$ v správnom tvare.

    \item $A=B \implies C$. Na $B,C$ platí IP a teda existujú formuly
        $B',C'$ v prenexnom tvare, pre ktoré platí
        $\provable B \lequiv B'$, $\provable C \lequiv C'$.
        Nech $A' = B' \implies C'$. Na základe vety o ekvivalencii platí
        $\provable A \lequiv A'$. Teraz potrebujeme dostať
        $A'$ do prenexného tvaru.
        Vezmime variant $C''$ formuly $C'$ taký, že $B',C''$ nemajú
        žiadnu spoločnú premennú.
        \begin{equation*}
            \provable A \lequiv (B' \implies C'')
        \end{equation*}
        Teraz použijeme prenexné operácie c), d) a formulu
        $B' \implies C''$ prevedieme do prenexného tvaru.

    \item $A=(\forall x)B$. Z indukčného predpokladu vyplýva
        existencia $B'$, $\provable B \lequiv B'$.
        Môžu nastať 2 prípady
        \begin{itemize}
        \item $x$ nie je viazaná v $B'$. Položme $A' = (\forall x) B'$
        \item $x$ je viazaná v $B'$. Potom máme $A' = B'$.
        \end{itemize}
\end{itemize}
%%% }}}
\end{dokaz}
\begin{poznamka}
    Ak $A$ obsahuje spojky 
    $\land,\lor$, môžeme použiť prenexnú operáciu e) alebo formulu nahradiť
    ekvivaletnou formulou obsahujúcou $\neg,\implies$.
    Ak sa vo vormule vyskytuje $\lequiv$, nemôžeme priamo
    použiť operácie e), d) ale $A\lequiv B$ prepíšeme na
    $(A\implies B) \land (B \implies A)$.
\end{poznamka}

\begin{priklad}
    \noindent
    Formula $A: B \lequiv (\forall x) C$ kde $x$ nie je voľná
    v $B$ a $y$ sa nevyskytuje v $B,C$.
    \begin{align*}
       (B \implies (\forall x) C) \land ((\forall x) C \implies B) &\\
       (B \implies (\forall x) C) \land ((\forall y) C_x[y] \implies B) 
       & \mbox{ -- podľa a)} \\
       (\forall x)(B \implies C) \land (\exists y) (C_x[y] \implies B) 
       & \mbox{ -- podľa c), d)} \\
       (\forall x)(\exists y)((B \implies C) \land (C_x[y] \implies B)
    \end{align*}
\end{priklad}

\begin{priklad}
    Formula elementárnej aritmetiky:
    \begin{align*}
        (\exists x) (x=y) \implies (\exists x)((x=0) \lor
                    \neg (\exists y)(y<0))& \\
        (\exists x) (x=y) \implies (\exists u)((u=0) \lor
                    \neg (\exists v)(v<0)) &\mbox{ -- podľa a)}\\
        (\exists x) (x=y) \implies (\exists u)((u=0) \lor
                    (\forall  v) \neg(v<0)) &\mbox{ -- podľa b)}\\
        (\exists x) (x=y) \implies (\exists u)(\forall v)
                ((u=0) \lor \neg(v<0)) &\mbox{ -- podľa e)}\\
        (\forall x)(\exists u)(\forall v) (x=y) \implies 
                ((u=0) \lor \neg(v<0)) &\mbox{ -- podľa c), d)}
    \end{align*}
\end{priklad}

